//this is the precondition for sum
/*@ n>=0 && n<5
 */
int sum (int n)
{
  int s, i;
  array[5, int] a;

  i=0;
  s=3;
  if(i<=n) 
  {
    a[1] = s+1;
    a[1] = 1;
    /*    a[2] = a[1] + 1;
	  a[3] = a[1] + a[2];*/
  }
  return a[1];
}
/*@  result == 1
 */
//this is the post-condition for sum

